Friday Code and Notes (Week 2)

1. Promela code
2. Notes

1 Promela code

1.1 Attempt 1

#define MutexDontCare
#include "critical2.h"

bit turn = 0;

proctype P() {
  do
  :: non_critical_section();
waitp: turn == 0;
csp: critical_section();
     turn = 1
  od
}
proctype Q() {
  do
  :: non_critical_section();
waitq: turn == 1;
csq: critical_section();
     turn = 0
  od
}

init { run P(); run Q(); }

ltl mutex { always !(P@csp && Q@csq)}
ltl waitp { [] (P@waitp implies (<> P@csp))  }
ltl waitq { [] (Q@waitq implies (<> Q@csq))  }

1.2 Attempt 2

#define MutexDontCare
#include "critical2.h"

bit wantp = 0;
bit wantq = 0;

proctype P() {
  do
  :: non_critical_section();
waitp: wantq == false;
     wantp = true;
csp: critical_section();
     wantp = false;
  od
}
proctype Q() {
  do
  :: non_critical_section();
waitq: wantp == false;
     wantq = true;
csq: critical_section();
     wantp = true;
  od
}

init { run P(); run Q(); }

ltl mutex { [] !(P@csp && Q@csq)}
ltl waitp { [] (P@waitp implies (eventually P@csp))  }
ltl waitq { [] (Q@waitq implies (<> Q@csq))  }

1.3 Attempt 3

You can do safety verification with "invalid endstates" enabled to find the deadlock here.

#define MutexDontCare
#include "critical2.h"

bit wantp = 0;
bit wantq = 0;

proctype P() {
  do
  :: non_critical_section();
     wantp = true;
waitp: wantq == false;
csp: critical_section();
     wantp = false;
  od
}
proctype Q() {
  do
  :: non_critical_section();
     wantq = true;
waitq: wantp == false;
csq: critical_section();
     wantq = false;
  od
}

init { run P(); run Q(); }

ltl mutex { [] !(P@csp && Q@csq)}
ltl waitp { [] (P@waitp implies (eventually P@csp))  }
ltl waitq { [] (Q@waitq implies (<> Q@csq))  }

1.4 Attempt 4

#define MutexDontCare
#include "critical2.h"

bit wantp = 0;
bit wantq = 0;

proctype P() {
  do
  :: non_critical_section();
waitp: wantp = true
     do
     :: wantq -> 
          wantp = false;
          wantp = true;
     :: else ->
          break
     od
csp: critical_section();
     wantp = false;
  od
}
proctype Q() {
  do
  :: non_critical_section();
waitq: wantq = true
     do
     :: wantp -> 
          wantq = false;
          wantq = true;
     :: else ->
          break
     od
csq: critical_section();
     wantq = false;
  od
}

init { run P(); run Q(); }

ltl mutex { [] !(P@csp && Q@csq)}
ltl waitp { [] (P@waitp implies (eventually P@csp))  }
ltl waitq { [] (Q@waitq implies (<> Q@csq))  }

1.5 Attempt 5

Attempt 5 is Dekker's algorithm, the first known correct solution to the critical section problem.

To verify eventual entry, you need to enable weak fairness to rule out traces where, after entering the pre-protocol, a process is never scheduled.

#define MutexDontCare
#include "critical2.h"

bit wantp = 0;
bit wantq = 0;
bit turn = 0;

proctype P() {
  do
  :: non_critical_section();
waitp: wantp = true
     do
     :: wantq -> 
       if
       :: turn == 1 -> 
            wantp = false;
            turn == 0;
            wantp = true;
       :: else -> skip
       fi
     :: else -> break
     od
csp: critical_section();
     turn = 1;
     wantp = false;
  od
}

proctype Q() {
  do
  :: non_critical_section();
waitq: wantq = true
     do
     :: wantp -> 
          if
          :: turn == 0 -> 
               wantq = false;
               turn == 1;
               wantq = true;
          :: else -> skip
          fi
     :: else -> break
     od
csq: critical_section();
     turn = 0;
     wantq = false;
  od
}

init { run P(); run Q(); }

ltl mutex { [] !(P@csp && Q@csq)}
ltl waitp { [] (P@waitp implies (eventually P@csp))  }
ltl waitq { [] (Q@waitq implies (<> Q@csq))  }

1.6 Critical section boilerplate

The above files use a critical2.h header file, whose contents are as follows.

/* 
  Definitions for critical section; derived from Ben-Ari's.

  If PID is defined, prints _pid in CS, otherwise prints a character parameter.

  If MutexDontCare is defined, no assertion is made about the number of
  processes in their CSs.
*/

#ifndef MutexDontCare
byte critical = 0; 
#endif
#define PID
#ifdef PID
inline critical_section() {
     printf("MSC: %d in CS\n", _pid);
#else
inline critical_section(proc) {
     printf("MSC: %c in CS\n", proc);
#endif
#ifndef MutexDontCare
     critical++;
     assert (critical == 1);
     critical--;
#endif
}

/* 
  Definitions for non-critical sections to complement M Ben-Ari's
  critical.h. If PID is defined, prints _pid in non-CS, otherwise
  prints its mandatory character argument.
*/

#ifdef PID
inline non_critical_section() {
  printf("MSC: %d in non-CS\n", _pid);
#else
inline non_critical_section(proc) {
  printf("MSC: %c in non-CS\n", proc);
#endif
  do                            /* non-deterministically choose how
                                   long to stay, even forever */
    :: true ->
         skip
    :: true ->
         break
  od
}

2 Notes

In a transition label

  g; f

when g = ⊤, we just write f

When there's no state update (when f = I "the identity function"),
then we write g

Q: do we allow Σ to be infinite? Yes.

Σ is the set of all possible states.

What is a state?
A: we don't bother specifying, because it's application dependent
  usually, at least:
  - a mapping from variable names to values
  - which location every process is at

Q: when we change the state, we also update the location, right?
   or: when we change the location, we change the state?
A: yes


== Floyd's method on the first transition diagram

P stands for the whole transition diagram.
   aka the triangular number program

We want to prove this Hoare triple:

  {⊤} P {s = N*(N-1)/2}

We must find an *annotation* for every location.
The annotation should state something that's
always true when we're at that location.

1 The precondition implies the
  start location's annotation
2 The exit location's annotation
  implies the postcondition.
3 If the current location's annotation is true,
  then if we take a transition, the next
  location's annotation becomes true.

Annotations (this is called an *assertion network*)

l0: ⊤
l1: i = 0
l2: s = i*(i-1)/2
l3: s = i*(i+1)/2
l4: s = N*(N-1)/2

Observe: the first two points above are trivial

Examples of point 3.

Consider the transition from l1 to l2.
We must prove
  i = 0 ⇒ (s = i*(i-1)/2)[s:=0]

that is:

  i = 0 ⇒ (0 = i*(i-1)/2)  <-- trivial

Consider the transition from l2 to l3
We must prove

  s = i*(i-1)/2 ∧ i ≠ N ⇒ s+i = i*(i+1)/2

You can prove this with some basic arithmetic


Q(l_i) ∧ g ⇒ Q(l_j) o f

o denotes function composition.

(f o g)(x) = f(g(x))

"If the annotation at l_i is true,
 and the guard is true,
 then, after updating the state with f,
 the annotation at l_j is true"



p1: wantp = 0                   
p2: wantp = 0
p3: wantp ≠ 0
p4: wantp ≠ 0 ∧ wantq ≠ wantp
p5: ⊤

q1: wantq = 0                   
q2: wantq = 0
q3: wantq ≠ 0
q4: wantq ≠ 0 ∧ wantp ≠ -wantq
q5: ⊤

Step 1: check that these annotations are inductive (separately)
Step 2: check for interference

  Suppose P is sitting at location p1. Therefore, wantp=0.
  We need to check that no action that Q could take
  falsifies wantp=0. Trivial because Q never changes wantp.

  Suppose instead P is sitting at p4.

   wantp ≠ 0 ∧ wantq ≠ wantp

  We need to check that nothing Q can do falsifies this annotation.
  There are two actions that are relevant are q2 and q5.

  For q5:

    wantp ≠ 0 ∧ wantq ≠ wantp ∧ ⊤ ⇒ wantp ≠ 0 ∧ 0 ≠ wantp (trivial)

  For q2:

    wantp ≠ 0 ∧ wantq ≠ wantp ∧ wantq = 0 ∧ wantp = -1 ⇒ wantp ≠ 0 ∧ 1 ≠ wantp
   ..and one more.


One final step: mutual exclusion holds.
  Show that  the annotations of p4 and q4 cannot both be true.
  Not possible because if so, wantp and wantq would have
  simultaneously different and equal polarity.